(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () Int)
(declare-fun var4 () Int)
(declare-fun var5 () Int)
(declare-fun var6 () Bool)
(declare-fun var7 () Bool)
(declare-fun var8 () Bool)
(assert (str.in.re (str.replace var2 var2 var1) (re.+ re.allchar)))
(assert (str.suffixof (str.substr var1 var3 var4) (str.replace var2 var2 var2)))
(assert (<= var4 var4))
(assert (str.suffixof (str.replace (str.replace var2 var0 var1) (str.at "`Fl*Zg{y@A" 6) (str.substr var2 (str.len (str.replace var0 var1 var2)) (str.len (str.replace var0 var2 var0)))) (str.substr (str.substr var0 var5 3) (str.len var0) (str.len var0))))
(check-sat)
